Circuit designers must verify the performance of newly-designed circuits. To aid the designer, Electronic Design Automation (EDA) tools from companies such as Synopsys, Cadence Design Systems, and Mentor Graphics, the assignee of the present invention, simulate and formally verify circuits described at the register transfer level (RTL) level using languages such as Verilog and VHDL.
One problem that has long confronted circuit designer is the verification of the effects of metastability in a circuit containing signals that cross clock domains. One such circuit where metastability may arise is illustrated in conjunction with FIG. 1A, which shows a prior art circuit 100 containing two portions 101 and 102 and a path 104 that carries a signal from portion 101 to portion 102. Path 104 may pass through any amount of combinational logic 199 (formed of logic elements but no storage elements). Registers in one portion 102 are clocked by a clock signal on a path 105 whereas registers in the other portion 101 are clocked by another clock signal on a different path 106. Note that the two clock signals on the two paths 105 and 106 are different from one another, which makes the two portions 101 and 102 into two different clock domains, hereinafter referred to as transmit clock domain 101 and receive clock domain 102. The difference in clock signals on paths 105 and 106 can be a difference in only frequency or only phase or both. For example, the clock signals on path 105 and 106 may have the respective frequencies 50 MHz and 37 MHz. A signal on path 104 crosses from clock domain 101 to clock domain 102, and hence this signal (on path 104) is hereinafter called a clock-domain-crossing (“CDC”) signal.
Although circuit 100 is illustrative of one clock-domain-crossing signal it is well known to the skilled artisan that today's integrated circuits have 100s of 1000s of such clock-domain-crossing signals and have 100s of clock domains. Moreover, the clock-domain-crossing signal on path 104 may pass through any amount of combinational logic 109 when traveling from transmit domain 101 to receive domain 102. Combinational logic 109 typically consists of any number of logic elements that are not clocked (i.e. there are no storage elements therein).
Each of portions 101 and 102 of circuit under verification 100 may contain any number of and any kind of circuit elements, e.g. storage elements that need to be clocked such as flip flops, as well as logic elements such as XOR gates and AND gates. For example, FIG. 1B shows a register 111 in the receive clock domain 102 of the circuit 100 of FIG. 1A. The D input of the register 111 of FIG. 1B is connected to the path 104 of FIG. 1A and therefore receives the clock-domain-crossing signal from domain 101. Moreover, the Q output of the register 111 of FIG. 1B generates a signal RX_Q that may be provided to any additional circuitry 191 in receive clock domain 102.
FIG. 1C shows another register 112 that is located in the transmit clock domain 101 of the circuit 100 of FIG. 1A. Register 112 has a Q output which drives the clock-domain-crossing signal on path 104. The D input of the register 112 of FIG. 1C receives a signal TX_D from any additional circuitry 192 in the transmit clock domain 101. The above-described additional circuitry 191 and 192 are each normally clocked by their respective clock signals on paths 105 and 106 respectively (and for this reason they belong to their respective clock domains).
It is well known in the art to verify the functional behavior of circuit 100 (which is also referred to as “circuit-under-verification”), based on a circuit description, by use of conventional register-transfer-level (hereinafter, RTL) simulators such as VCS (from Synopsys, Inc.) and Verilog NC (from Cadence Design Systems, Inc.). The circuit description for circuit 100 is normally articulated by a circuit designer in a Hardware Description Language (HDL), such as Verilog. Note that instead of a Verilog representation, circuit 100 may be described in any other HDL, such as VHDL, or in an internal representation (such as a graph structure or a net list structure) in a programmed computer as will be apparent to the skilled artisan.
A designer of circuit 100 may additionally articulate a description of one or more assertions that monitor various signals in circuit 100 that normally occur during simulation. The assertions (also called “checkers”) are articulated to generate error signals when a certain combination of signals in circuit 100 cause a condition specified in the assertion to be violated during simulation. Assertions can receive signals from either or both portions 101 and 102 of circuit 100, depending on the assertion.
FIG. 1A illustrates an assertion 103 that receives input signals on paths 108 and 107 respectively from each of the two clock domains 101 and 102. Note that paths 107 and 108 are shown dashed in FIG. 1A to indicate that the paths are not necessarily present in a circuit description, e.g. assertion 103 may receive signals only on path 108 or only on path 107 or on both paths 107 and 108 depending on the circuit design and/or the assertion. For more information on assertions, see U.S. Pat. Nos. 6,175,946 and 6,609,229 granted to Ly et al that are incorporated by reference herein in their entirety.
During simulation of circuit 100 (FIG. 1A) with conventional RTL simulators, assertion 103 does not receive certain signals that result from the effects of metastability, because metastability is not modeled explicitly in prior art systems. In contrast, metastability effects are known to arise in physical implementations of circuit 100, due to the difference in the two clock signals on paths 105 and 106. Specifically, a physical register implemented in silicon, for example, the register in FIG. 1B that receives the clock-domain-crossing signal of FIG. 1A, is characterized by parameters called “setup time” and “hold time”. If a signal at the data input of the physical register changes logic values within the setup time before the active edge of the register's clock signal, or within the hold time after the active edge of the register's clock signal, then the output of the register becomes unpredictable, and may settle to either logic value 1 or logic value 0. For more information, see “Digital Systems Engineering,” Dally, W. J., and Poulton, J. W., Cambridge Univerity Press, 1998, pp. 462-513.
A clock-domain-crossing signal on path 104 changes its logic value during the setup time or during the hold time of register 111 in the receive clock domain 102 due to the relative difference in times at which the two clock domains 101 and 102 are clocked by their respective clock signals on paths 106 and 105. FIGS. 2A and 2B show representative electrical waveforms for the output of a physical register in the physical world that has been implemented in silicon (as an integrated circuit die), in situations where the clock-domain-crossing signal violates the setup time of this register 111.
In FIG. 2A, a signal at the output of register 111 initially goes only part way to logic level 1 and then settles to logic level 0 whereas in FIG. 2B the same signal initially goes only part way to logic level 1 and then settles to logic level 1. Similarly, FIGS. 2C and 2D show the corresponding electrical waveforms when the hold time of the physical register 111 is violated and the output signal settles to logic level 1 and logic level 0 respectively. The logic level to which a signal settles in the physical world i at the output of a physical register 111 depends on a number of factors (such as thermal effects and/or voltages) that are not normally modeled in conventional RTL simulation.
FIGS. 3A and 3B show representative simulation waveforms produced by conventional RTL simulation of the circuit 100 of FIG. 1A in cases where a signal at the data input of a register 111 in the receive clock domain 102 violates the setup time and hold time parameters. As can be seen by comparing FIG. 3A with FIGS. 2A and 2B and by comparing FIG. 3B with FIGS. 2C and 2D, the electrical waveforms of the physical register may differ from the simulation waveforms produced by conventional RTL simulation when the setup or hold time parameter of the register is violated. Note that only one outcome is produced by the RTL simulator when the setup time is violated as shown in FIG. 3A. Similarly only one outcome is produced when the hold time is violated as shown in FIG. 3B. The outcome produced by the RTL simulator is also called the “correct” logic value, and the inversion of the outcome produced by the RTL simulator is also called the “incorrect” logic value.
In contrast, when a signal at the data input of a physical register in the physical world changes logic values within the setup time before the active edge of the register's clock signal, then the signal at the output of the physical register in the physical world may settle to either a “correct” logic value (i.e., a value matching the value produced by conventional RTL simulation of the register), or an “incorrect” logic value (i.e., the inversion of the value produced by conventional RTL simulation of the register), as shown in FIGS. 2A and 2B. Similarly, two outcomes are possible when the signal changes within the hold time after the active edge of the register's clock signal, as shown in FIGS. 2C and 2D.
An example circuit 400 shown in FIG. 4A is similar or identical to the corresponding circuit 100 described above, except for the following differences. The reference numerals in FIG. 4A are obtained from the corresponding reference numerals in FIG. 1A by adding 300. Circuit 400 includes multiple paths (e.g. n paths) in a bus 404 between the two clock domains 401 and 402. In this example, the n-bit signal on bus 404 that crosses clock domains 401 and 402 happens to have been designed by the circuit designer to be one-hot, which satisfies the property that exactly one bit of the n-bit signal is asserted at all times during normal operation.
Note that in circuit 400 of FIG. 4A, assertion 403 is coupled to only the receive clock domain 402 to receive therefrom a version of the n-bit signal after it has been clocked in by receive clock domain 402 (which receives this signal on path 404 from transmit clock domain 401). Assertion 403 may be articulated by the designer of circuit 400 to be a one-hot assertion which checks that the signal on path 407 is in fact one hot (i.e. that exactly one bit of the n-bit signal is asserted at all times). Assertion 403 contains an XNOR gate 421 that receives signals RX_Q_1 and RX_Q_0 that are output by registers 411_1 and 411_0. XNOR gate 421 supplies an error signal when its inputs are the same and this error signal is latched in a register 422 also included in assertion 403. Note that assertion 403 is not connected to transmit clock domain 401 in this example although in other examples such an assertion may be connected to only transmit clock domain 401, or to both clock domains.
An example of circuit 400, for n=2, is described next, in reference to FIG. 4B. Transmit clock domain 401 contains two registers that form a one-hot counter 412 (see registers 412_1 and 412_0, together called “tx_reg”). Counter 412 is clocked by the rising edge of the transmit clock signal TX_CLK. When the reset signal RST, is asserted, register 412_1 is set to 0 (deasserted) and register 412_0 is set to 1 (asserted). At each rising edge of the transmit clock signal TX_CLK after the reset signal RST is deasserted, the values stored in registers 412_1 and 412_0 are swapped. Therefore, the counter 412 (called “tx_reg” which is a short form for “transmitting register”) remains one-hot at all times after reset.
In the example circuit of FIGS. 4B and 4C, the one hot signal from tx_reg counter 412 (i.e. from registers 412_1 and 412_0) is clocked into a counter 411 (formed by registers 411_1 and 411_0 that are together called “rx_reg” which is a short form for “receiving register”), on each rising edge of receive clock signal RX_CLK. As described above, since input signal TX_Q_0 is clocked into receiving register 411_0 by a first clock signal (RX_CLK), transmitting register 412_0 is in the combinational fanin of signal TX_Q_0, and register 412_0 is clocked by a second clock signal (TX_CLK), it follows that signal TX_Q_0 is a clock-domain-crossing (“CDC”) signal. Note that signal TX_Q_0 transmitted by the transmit clock domain 401 on path 404_0 is same as signal RX_D_0 that is received by the receive clock domain 402 at the D input of register 411_0. In a similar manner, note that signal TX_Q_1 is a CDC signal also, and is same as signal RX_D_1 received at the D in put of register 411_1.
A Verilog representation of circuit 400 of FIG. 4B is shown in Appendix A, which is located just before the claims in this patent application. Appendix A is an integral portion of this background section of this patent application, and is incorporated by reference herein in its entirety. For a description of the Verilog language, see “The Verilog Hardware Description Language, Second Edition” Thomas, D. E., and Moorby, P. R., Kluwer Academic Publishers, 1995. In the Verilog of FIG. 4B, registers 411_1, 411_0, 412_1 and 412_0 are represented as rx_reg_1, rx_reg_0, tx_reg_1, and tx_reg_0 respectively. Moreover, signal names shown in upper case letters in FIG. 4B are replaced by corresponding names in lower case letters in Appendix A. Note that the initial state represented in the initial block of the Verilog shown in Appendix A corresponds to the reset state of the circuit under verification, i.e., tx_reg_1=0, tx_reg_0=1, rx_reg_1=0, and rx_reg_0=1.
As noted above, circuit 400 of FIG. 4B contains assertion 403 to check that the value stored in the rx_reg counter 411 is in fact one-hot (see lines 42-44 in Appendix A). The output of the one-hot assertion 403 becomes asserted when the assertion is “violated”, if and only if the value stored in rx_reg counter 411 is not one-hot at the rising edge of the receive clock signal RX_CLK. During conventional RTL simulation, a violation flagged by the one-hot assertion 403 indicates that the value of the rx_reg counter 411 is not one-hot.
The just-described error in the rx_reg counter 411 is treated by a circuit designer as an indication that an error occurred in the generation of the one-hot signal but not that the one-hot signal was corrupted during transmission across clock domains. This is because conventional RTL simulators such as VCS and NC Verilog do not accurately model metastability affecting the CDC signals. Therefore, during conventional RTL simulation of the example circuit 400 of FIG. 4B, the value of the tx_reg counter is modeled as being correctly transmitted to the rx_reg counter, regardless of the violation of setup times (of registers 411_0 and 411_1). For this reason, when the one-hot signal is correctly generated and stored in the tx_reg counter 412 the one-hot assertion 403 that monitors the signal on path 107 is not violated during conventional RTL simulation.
As noted above, RTL simulation in the conventional manner produces only one outcome (i.e. one logic level) in the event of a setup time violation although two outcomes are possible. Moreover, RTL simulation also produces only one outcome (i.e. one logic level) in the event of a hold time violation, although two outcomes are possible. The inventors believe there is a need to take into account the outcomes that are not conventionally produced by RTL simulation. Specifically, the inventors believe that explicit modeling of all outcomes could lead to detection of errors that are not otherwise detected by RTL simulation.
It is well known in the art that the real behavior of a circuit in hardware often differs from the predictions made by conventional RTL simulation because of various physical effects. Thus, a circuit design that is verified using conventional RTL simulation may still have hidden errors that will affect the behavior of the final hardware circuit. In particular, circuit designers cannot rely on conventional RTL simulation tools to accurately and reliably determine whether a complex circuit design is able to reliably function in the presence of metastability on the outputs of registers receiving clock-domain-crossing signals.
Incorporated by reference herein in its entirety as background is an article entitled “Using Assertion-Based Verification to Verify Clock Domain Crossing Signals” by Chris Ka-Kei Kwok, Vijay Vardhan Gupta and Tai Ly presented at Design and Verification Conference (DVCon 2003), February, 2003.